Inference at * 2 
Iof proof for Lemma adjacent-cons:



1. T : Type
2. x : T
3. y : T
4. u : T
5. L : T List
6. 0 < ||L||
7. (x = u & y = hd(L))  (i:{0..(||L|| - 1)}. (x = L[i] & y = L[(i+1)]))
  i:{0..((||L||+1) - 1)}. (x = [u / L][i] & y = [u / L][(i+1)]) 

latex

 by D (-1) 

latex

 1: 

 1: 7. x = u & y = hd(L)
 1:   i:{0..((||L||+1) - 1)}. (x = [u / L][i] & y = [u / L][(i+1)])
 2: 

 2: 7. i:{0..(||L|| - 1)}. (x = L[i] & y = L[(i+1)])
 2:   i:{0..((||L||+1) - 1)}. (x = [u / L][i] & y = [u / L][(i+1)])
 .

Definitions

P  Q, left + right